FDL - Step of Proof: nat_well_founded

Step of Proof: nat_well_founded

Inference at * 1 1 1
Iof proof for Lemma nat well founded:

1. P :

2.

j:

. (

k:

. (k < j)

P(k))

P(j)

n:

. (

j:

. (j < n)

P(j))

P(n)

by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)

.